
\section{The framework}


In this section we describe the syntax and the semantics of our framework. 


The main concepts are \emph{networks} and \emph{configurations}. Each network models the idea of a set of running units that interact together by establishing sessions and by exchanging messages. Each unit has a single task and it is implemented by a configuration. This way we could have units that models a client behavior, other that are servers, etc.
More formally,  a network ranged over by $N, M, \dots $is the restriction on a number of channels $\til{\kappa}$ of the parallel composition of a set of configurations:
$$
N::= \nil \mid C \parallel C \mid \nu \til{\kappa}~ C 
$$

A configuration (ranged over by $C, D, \dots$) located at $l$ is composed by three parts $ \tuple{l}{P}{S}{M}$: a process $P$ that implements the actual task of the unit together with some management procedures that will be made clear later; a state $S$ that stores information on the channels used by the configuration, and finally a memory $M$  that is used to store recovering points.
The intuition behind configurations is that of a process that runs independently establishing sessions either internally or with other configurations/units.  
An internal session represents a task that is implemented internally to the same unit: i.e. both endpoints belong to the same configuration. An external session is represented by the interaction of two configurations: for instance one configuration plays the role of a server offering certain services while the other is a client requesting one of those services. 
Inside configurations the manager or handler is able to detect problematic/error situations and to handle them.
This way the manager is able, for instance, to stop/restart the current computation or to consistently rollback to a given recovering point in the memory.
Hence,  a process is the parallel composition of a handler $\manager$ and a number of running items $\local{\til{\kappa}}{R}$, where $R$ is a process given in the session language in Table \ref{tab:sessionlan} and $\til{\kappa}$ is the nesting of established sessions in $R$: 
$$
\begin{array}{ll}
 P::= &               \nil ~\mid~  \local{\til{\kappa}}{R} ~\mid~ \manager ~\mid~ P | P  \\
\manager ::= &  \queue{\kappa^p}{\msg} \mid \act{\til{\kappa}} \mid \dots \\
\msg ::= & stop \mid \dots
\end{array}
$$

Then  $S$ is a collection of channels states $\state{\kappa^p}{T}{q}$ where $\kappa^p$ is the name of the channel with its polarity\footnote{It is necessary to store the polarity as we could have both ends of the channel in the same configuration (internal session).}, $T$ is the ``runtime'' type of the session in $\kappa$, and $q$ is a queue where we store special messages  $\msg$ that are sent by  $\manager$ via the $\queue{\kappa^p}{\msg}$ operator  and that are used to perform management actions on the session.  
$$
\begin{array}{ll}
 S ::= & \emptyset \mid \state{\kappa^p}{T}{q},S \\
 q::= & \varepsilon \mid q \cdot \msg
\end{array}
$$


Finally, the memory $M$ is a tree of nodes $\node{\til{\kappa}}{R}{S}$ that represent recovering points. Intuitively each recovering point is labeled by the unique sequence  $\til{\kappa}$ and the node contains further information on the form of the process $R$  and on the state $S$. 
 The intuition is that along the evolution of the process $P$ we will save into the memory some particular states, e.g. before establishing a session, and we will use these recovering points for management. When requested by the manager via the special operation  $\act{\til{\kappa}}$ we will stop the current computation and substitute the current running process and state with the process $\local{\til{\kappa}}{R}$ together with the associate state $S$ thus restoring the behavior of the configuration at the recovering point $\til{\kappa}$.
We assume implemented the usual operations of insertion of nodes ($\addchild{\til{\kappa}}{node}$: add  $node$ to the node labeled with $\til{\kappa}$) and removal of subtrees rooted at a given node ($M(label) \pired M(\emptyset)$).

Note: CREDO CHE LE ETICHETTE DEI NODI SI POSSANO ACCORCIARE, ANZICHE' TUTTO IL PERCORSO SONO L'ULTIMA SESSIONE APERTA

(CHE ABBIA SENSO AGGIUNGERE AL MANAGER UN OPERAZIONE DI SAVE CURRENT STATE??)


\begin{table}[t]
 $$
\begin{array}{lrlr}
R & ::=  &   \request{a}{x:T}.R  & \text{session request}	\\
	& \sepr &   \accept{a}{x:T}.P  & \text{session acceptance: linear}	\\
	       & \sepr & \raccept{a}{x:T}.P  & \text{session acceptance: persistent}	\\
	& \sepr &  \outC{k}{\tilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\tilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{k'}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    	&\sepr&   \branch{k}{n_1{:}P_1 \parallel \cdots \parallel n_m{:}P_m} & \text{branching}\\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{arithmetic expressions}
\end{array} 
$$
 \caption{Syntax for sessions}\label{tab:sessionlan}
\end{table}





\begin{table}[ht]
$$
\begin{array}{ll}
\text{Network} & N::= \nil \mid C \parallel C \mid \nu \til{\kappa}~ C \\

\text{Configuration:}  &  C :: = \tuple{P}{S}{M}{l} \\

\text{Process:} &  P::=       \nil \mid  \local{\til{\kappa}}{R} \mid \manager \mid P | P  \\
\text{Manager:} & 
\manager ::= \queue{\kappa^p}{\msg} \mid \act{l_{\til{\kappa}}} \mid \dots \\  
\text{State:} & S ::= \emptyset \mid \state{\kappa^p}{T^{\til{\kappa}}}{q},S\\

\text{Queue:} & q::=\varepsilon \mid q \cdot \msg  \\

\text{Messages:} & \msg ::=  stop \mid \dots \\

\text{Memory:} & \text{Tree of nodes } \node{\til{\kappa}}{R}{S} \\

\text{Sessions:} & \text{Your favourite language for sessions}

 
\end{array}
$$
\caption{Framework syntax} \label{tab:all}
\end{table}


Next section will make more precise the intuitions on the semantics given here.

\section{Semantics}
As hinted at above our configurations manage both internal and external sessions, this way we need to duplicate the semantics of each operator into a global semantics that refers to sessions established between two configurations and a local semantics that deals with internal sessions (i.e. sessions established within the configuration).
We explain in detail only the case of the global semantics, local semantics is analogous.

\paragraph{Global operational semantics}
We start with session establishment: 
$$
\begin{array}{l}
  \mathbf{Connect}\\
 \tuple{l}{\local{\til{\kappa_1}}{\accept{a}{x:T}.P_1}}{S_1}{M_1} \parallel 
  \tuple{n}{\local{\til{\kappa_2}}{\request{a}{y:\overline{T}}.P_2}}{S_2}{M_2} 
 \pired   \\
 \quad \nu \kappa~ ( 
 \tuple{l}
  {\local{\til{\kappa_1}\cdot \kappa^+}{P_1\subst{\kappa^+}{x}}}
  {S_1, \state{\kappa^+}{T}{\varepsilon}}
  {M_1  \addchild{\til{\kappa_1}}{\node{\til{\kappa_1}\cdot \kappa^+}{\accept{a}{x:T}.P_1}{S_1\downarrow_{P_1, \til{ \kappa_1}}} }}  \parallel \\

\qquad \ \ \ \tuple{n}
   {\local{\til{\kappa_2}\cdot \kappa^-}{P_2\subst{\kappa^-}{y}}}
   {S_2, \state{\kappa^-}{\overline{T}}{\varepsilon}}{M_2\addchild{\til{\kappa_2}}{\node{\til{\kappa_2}\cdot \kappa^-}{\request{a}{y:\overline{T}}.P_2}{S_2\downarrow_{P_2, \til{ \kappa_2}}}}  } )
\end{array}
$$
where 
$S \downarrow_{P, \til{\kappa}}$ is the selection of queues in state $S$ restricted to channels $\iota$ in the set $\{\iota \mid \iota \in fn(P_1) \wedge \iota \in \til{\kappa_1}\}$.

Upon session establishment, as in standard session languages, we create a fresh channel $\kappa$ and assign one end of the channel of each configuration. On each configuration, we update each unit adding the name of the channel of the session $\local{\til{\kappa_1}\cdot \kappa^+}{\cdot}$ and  $\local{\til{\kappa_2}\cdot \kappa^-}{\cdot}$. Then in each of the states $S_1$ and $S_2$, we add  a new state $\state{\kappa^+}{T}{\varepsilon}$ ($\state{\kappa^-}{\overline{T}}{\varepsilon}$ respectively) where $T$ is the type of the session in $\kappa^+$ and $\varepsilon$ in an empty queue. Finally, as for transactions,  connection establishment represent an important step in the evolution of the process. For this reason, we save in both memories $M_1$ and $M_2$ the state of the process before the establishment of the session. 
We comment on the treatment of memory in  configuration $l$, configuration $n$ behaves symmetrically. 
Saving a restoring point consists in adding a new node $\node{\til{\kappa_1}\cdot \kappa^+}{\accept{a}{x:T}.P_1}{S_1\downarrow_{P_1, \til{ \kappa_1}}}$  to the node labeled $\til{\kappa_1}$. Notice that, in the state, we save only the channels that are effectively used by process $P_1$.

Below, notice that $\kappa \in \iota$
$$
\begin{array}{l}
\rulename{r:I/O} \\
\tuple{l}{\local{\til{\iota_1}}{\outC{\cha^{p}}{\tilde{e}}.P_1}}{S_1, \state{\kappa^p}{!(\tilde{\capab}).\alpha}{q_1}}{M_1} \parallel 
\tuple{n}
{\local{\til{\iota_2}}{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_2}}
{S_2, 
\state{\kappa^{\overline{p}}}{?(\tilde{\capab}).\overline{\alpha}}{q_2}}
{M_2} \pired 
\\ \qquad 
\tuple{l}{\local{\til{\iota_1}}{P_1}}{S_1, \state{\kappa^p}{\alpha}{q_1}}{M_1} \parallel 
\tuple{n}
{\local{\til{\iota_2}}{P_2\subst{\til{e}}{\til{x}}}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha}}{q_2}}
{M_2} \quad (\kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\

 \rulename{r:Pass} \\
\tuple{l}
{\local{\til{\kappa_0}\cdot \kappa_1^p \cdot \til{\kappa_2}\cdot \kappa_3 \cdot \til{\kappa_4}}{\throw{\cha_1^{p}}{\kappa_3}.P_1}}{S_1, \state{\kappa_1^p}{!\beta.\alpha}{q_1}, \state{\kappa_3}{\beta}{q_1'}}{M_1} \parallel  \\
\tuple{n}
{\local{\til{\iota_0}\cdot \kappa^{\overline{p}} \cdot \til{\iota_1}}{\catch{\cha^{\overline{p}}}{x}.P_2}}
{S_2, 
\state{\kappa^{\overline{p}}}{?\beta.\overline{\alpha}}{q_2}}
{M_2} \pired 
\\ \qquad 
\tuple{l}{\local{\til{\kappa_0}\cdot \kappa_1^p \cdot \til{\kappa_2}\cdot \kappa_3 \cdot \til{\kappa_4}}{P_1}}{S_1, \state{\kappa^p}{\alpha}{q_1}}{M_1} \parallel 
\\ \qquad
\tuple{n}
{\local{\til{\iota_0}\cdot \kappa^{\overline{p}} \cdot \til{\iota_1} \cdot \kappa_3}{P_2\subst{\kappa_3}{x}}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha}}{q_2},
 \state{\kappa_3}{\beta}{q_1'}}
{M_2'}\\
\text{where } M_2' =M_2 \addchild{\til{\iota_0}\cdot \kappa^{\overline{p}} \cdot \til{\iota_1}}
                        {\node{\til{\iota_0}\cdot \kappa^{\overline{p}} \cdot \til{\iota_1} \cdot \kappa_3}{\catch{\cha^{\overline{p}}}{x}.P_2}{S_2'}} 
\\ \qquad \ \ \ 
S_2' = \{S_2, 
 \state{\kappa^{\overline{p}}}{?\beta.\overline{\alpha}}{q_2}
\}\downarrow_{\catch{\cha^{\overline{p}}}{x}.P_2, \til{\iota_0}\cdot \kappa^{\overline{p}} \cdot \til{\iota_1} }\\
\\

 \rulename{r:Sel} \\
\tuple{l}
{\local{\til{\iota_1}}{\branch{\cha^{p}}{h_1{:}P_1 \parallel \cdots \parallel h_m{:}P_m}}}
{S_1, \state{\kappa^p}{ \&\{h_1:\alpha_1, \dots,  h_m:\ST_m \}}{q_1}}{M_1} \parallel \\
\tuple{n}
{\local{\til{\iota_2}}{\select{\cha^{\overline{p}}}{h_j};Q}}
{S_2, 
\state{\kappa^{\overline{p}}}{\oplus\{h_1:\overline{\alpha_1}, \dots , h_m:\overline{\ST_m} \} }{q_2}}
{M_2} \pired 
\\ \qquad 
\tuple{l}{\local{\til{\iota_1}}{P_j}}{S_1, \state{\kappa^p}{\alpha_j}{q_1}}{M_1} \parallel 
\tuple{n}
{\local{\til{\iota_2}}{Q}}
{S_2, 
\state{\kappa^{\overline{p}}}{\overline{\alpha_j}}{q_2}}
{M_2} \\
\hfill (1 \leq j \leq m,~  \kappa^p \in \iota_1 \text{ and } \kappa^{\overline{p}} \in \iota_2)  \\
\\
 \rulename{r:Close} \text{DA DISCUTERE} \\
\tuple{l}{\local{\til{\iota_1}\cdot \kappa^p}{\close{\cha^{p}}.P_1}}{S_1, \state{\kappa^p}{\varepsilon}{q_1}}{M_1(\til{\iota_1}\cdot \kappa^p)} \parallel \\
\tuple{n}
{\local{\til{\iota_2}\cdot \kappa^{\overline{p}}}{\close{\cha^{\overline{p}}}.P_2}}
{S_2, 
\state{\kappa^{\overline{p}}}{\varepsilon}{q_2}}
{M_2(\til{\iota_1}\cdot \kappa^{\overline{p}})}  \pired 
\\ \qquad
\tuple{l}{\local{\til{\iota_1}}{P_1}}{S_1}{M_1(\emptyset)} \parallel 
\tuple{n}
{\local{\til{\iota_2}}{P_2}}
{S_2, }
{M_2(\emptyset)} 
\end{array}
$$

notes: NELLA DELEGATION BISOGNA TRASFERIRE ANCHE LA CODA Q' DI K3?? IO DIREI DI SI

IO PERMETTEREI LA CLOSE SOLO ALLE SESSIONI TOP LEVEL



$$
\begin{array}{l}
\mathbf{Queue}  \\
\tuple{l}{\queue{\kappa^p}{\msg}.P_1}{S_1}{M_1}
\parallel 
\tuple{n}{P_2}{S_2,\state{\kappa^p}{T}{q}}{M_2}
\pired \\
\quad 
\tuple{l}{P_1}{S_1}{M_1}
\parallel 
\tuple{n}{P_2}
 {S_2,\state{\kappa^p}{T}{q \cdot \msg}}
 {M_2}

\end{array}
$$




\paragraph{Local operational semantics}

$$
\begin{array}{l}
  \mathbf{Connect}\\
 \tuple{l}
{\local{\til{\kappa_1}}{\accept{a}{x:T}.P_1} \mid 
  \local{\til{\kappa_2}}{\request{a}{y:\overline{T}}.P_2}
}{S}{M}  \pired   \\
 \ \nu \kappa  \langle \ 
  {\local{\til{\kappa_1}\cdot \kappa^+}{P_1\subst{\kappa^+}{x}} \mid 
\local{\til{\kappa_2}\cdot \kappa^-}{P_2\subst{\kappa^-}{y}}};\\

\qquad 
  {S, \state{\kappa^+}{T}{\varepsilon},
        \state{\kappa^-}{\overline{T}}{\varepsilon}};\\

\qquad 
  {M  \addchild{l_{\til{\kappa_1}}}{\node{\local{l}{\til{\kappa_1}\cdot \kappa^+}{\accept{a}{x:T}.P_1}}{S_1\downarrow_{P_1, \til{ \kappa_1}}}}
\addchild{l_{\til{\kappa_2}}}{\node{\local{l}{\til{\kappa_2}\cdot \kappa^-}{\request{a}{y:\overline{T}}.P_2}}{S_2\downarrow_{P_2, \til{ \kappa_2}}}
} }\  \rangle_{l}  \\
\\
 \mathbf{Queue} \\
\tuple{l}
 {\queue{\kappa^p}{\msg}.P}
 {S,\state{\kappa^p}{T}{q}}
 {M}
\pired 
\tuple{l}
 {P}
 {S,\state{\kappa^p}{T}{q \cdot \msg}}
 {M}\\
\\
\mathbf{Activate}\\
\tuple{l}
{\local{\til{\kappa_0} \cdot \kappa_1\cdot \til{\kappa_2}}{P} \mid \act{\til{\kappa_0} \cdot \kappa_1}}
{S}
{M({\til{\kappa_0} \cdot \kappa_1})}
\pired 
\\ \qquad 
\tuple{l}
{\local{\til{\kappa_0} \cdot \kappa_1 }{P'}}
{S \setminus (S\downarrow_{P,\kappa_1 \cdot \til{\kappa_2}} \cup S\downarrow_{P,\til{\iota}} ) \cup S_{\til{\iota}} } 
{M(\emptyset)}\\
\\
 \rulename{r:IfTr} \\
% C\{\ifte{e}{P}{Q}\} \pired C\{P\}  \quad (e \downarrow \mathtt{true})  \vspace{ 1.5mm}
% \\
\rulename{r:IfFa} \\
% C\{\ifte{e}{P}{Q}\} \pired C\{Q\}  \quad (e \downarrow \mathtt{false}) \vspace{ 1.5mm}
% \\
% 


\end{array}
$$


where with $M(l_\kappa)$ we denote the node whose label start with $l_\kappa$ notice that we have just one of these nodes


Notes: why do not we use the command close of a session to sort of commit changes and free the memory of all objects created along the session?


\paragraph{Structural congruence rules and compositional rules}
The following are rules to handle parallel composition:
$$
\begin{array}{c}
 \cfrac
{\tuple{l}{P}{S}{C} \pired \tuple{l}{P'}{S'}{C'}}
{\tuple{l}{P|Q}{S}{C} \pired \tuple{l}{P'|Q}{S'}{C'}} \\
\\
\cfrac
{\tuple{l}{P_1}{S_1}{C_1} \pired \tuple{l}{P_1'}{S_1'}{C_1'}}
{\tuple{l}{P_1}{S_1}{C_1} \parallel \tuple{n}{P_2}{S_2}{C_2} \pired \tuple{l}{P_1'}{S_1'}{C_1'}\parallel \tuple{n}{P_2}{S_2}{C_2}} \\
\\
\cfrac
{N \pired N'}
{\nu \kappa N \pired \nu \kappa N'}
\\
\\
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q

\end{array}
$$



Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:
$$
\begin{array}{ll}
 !a(x).P \equiv !a(x).P | a(x).P &
\local{\til{\kappa}}{P | Q} \equiv \local{\til{\kappa}}{P } | \local{\til{\kappa}}{ Q}\\
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\cha}{\nil} \!\equiv\! \nil & \restr{\cha}{\restr{\kappa'}{P}} \!\equiv\! \restr{\cha'}{\restr{\cha}{P}} \\
\restr{\cha}{C} \!\para \! D \!\equiv\! \restr{\cha}{(C \!\para \! D)} ~~\text{(if $\cha \not\in \mathsf{fc}(D)$)}
\end{array}
$$

Notes: perche' la seconda regola di equiv strutturale non puo' essere simmetrica? negli appunti avevamo scritto $\Leftarrow$ e basta